00100		Here are some reactions to Milner's May 7 memo "Future work
00200	on LCF".
00300	
00400		1. The proposed recursively enumerable relation R(S,B) is
00500	not the most general form of rule of inference.  This would be
00600	some thing like R(S,B,P) where P is a generalized parameter.  The
00700	idea is that P contains whatever additional information is required
00800	to guarantee that B follows from S.  For example, P might specify
00900	a sequence of magic substitutions.  I can give more examples if
01000	necessary.
01100	
01200		2. I would like to choose priorities in such a way as will
01300	lead to a practically useful system for a useful class of programs
01400	as soon as possible.  I don't see that this can be done very quickly,
01500	but it would have a very large payoff in showing that theoretical
01600	work in MTC has genuine practical applications.  My other comments
01700	reflect this orientation.
01800